A:Dsys, i, a:Id. a declared in M(i)   

latex

Definitions	x:A. B(x), t  T, a declared in M, P  Q, t.1, t.2, , x. t(x), MsgA, Valtype(da;k), x(s)
Lemmas	Id wf, dsys wf, d-m wf, msga wf, assert wf, fpf-dom wf, Knd wf, Kind-deq wf, fpf-trivial-subtype-top, locl wf